Termination w.r.t. Q proof of /tmp/tmpsaFQxG/un12.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

The set Q is empty.
We have obtained the following QTRS:

b(a(b(b(a(b(a(b(b(b(x)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x)))))))))))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(a(b(a(b(b(b(x)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x)))))))))))))

Q is empty.

We were given the following TRS:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

By stripping symbols from the only rule of the system, we obtained the following TRS:

b(b(a(b(a(b(b(a(b(x1))))))))) → b(a(b(a(b(b(b(a(b(a(b(b(x1))))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

    ↳ QTRS

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(a(b(a(b(b(a(b(x1))))))))) → b(a(b(a(b(b(b(a(b(a(b(b(x1))))))))))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(x1))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(a(b(a(b(b(x1)))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(b(a(b(a(b(b(x1))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(a(b(b(b(a(b(a(b(b(x1))))))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(a(b(b(x1))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(b(x1))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(b(b(a(b(a(b(b(x1))))))))))

The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(x1))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(a(b(a(b(b(x1)))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(b(a(b(a(b(b(x1))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(a(b(b(b(a(b(a(b(b(x1))))))))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(a(b(b(x1))))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(b(x1))))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(a(b(b(b(a(b(a(b(b(x1))))))))))

The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(x1))
B(b(b(a(b(a(b(b(a(b(x1)))))))))) → B(b(b(a(b(a(b(b(x1))))))))

The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x1)))))))))))))

The set Q is empty.
We have obtained the following QTRS:

b(a(b(b(a(b(a(b(b(b(x)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x)))))))))))))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ Strip Symbols Proof

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(a(b(a(b(b(b(x)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x)))))))))))))

Q is empty.

We were given the following TRS:

b(a(b(b(a(b(a(b(b(b(x)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(b(x)))))))))))))

By stripping symbols from the only rule of the system, we obtained the following TRS:

a(b(b(a(b(a(b(b(b(x))))))))) → b(a(b(a(b(b(b(a(b(a(b(b(x))))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ Strip Symbols Proof

        ↳ QTRS

          ↳ RFCMatchBoundsTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a(b(b(a(b(a(b(b(b(x))))))))) → b(a(b(a(b(b(b(a(b(a(b(b(x))))))))))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(b(b(a(b(a(b(b(b(x))))))))) → b(a(b(a(b(b(b(a(b(a(b(b(x))))))))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

422, 423, 434, 433, 431, 432, 429, 430, 428, 427, 425, 426, 424, 445, 444, 442, 443, 440, 441, 439, 438, 436, 437, 435, 456, 455, 453, 454, 451, 452, 450, 449, 447, 448, 446, 467, 466, 464, 465, 462, 463, 461, 460, 458, 459, 457

Node 422 is start node and node 423 is final node.

Those nodes are connect through the following edges:

422 to 424 labelled b_1(0)
423 to 423 labelled #_1(0)
434 to 423 labelled b_1(0)
433 to 434 labelled b_1(0)
431 to 432 labelled b_1(0)
432 to 433 labelled a_1(0)
432 to 435 labelled b_1(1)
429 to 430 labelled b_1(0)
430 to 431 labelled a_1(0)
430 to 446 labelled b_1(1)
428 to 429 labelled b_1(0)
427 to 428 labelled b_1(0)
425 to 426 labelled b_1(0)
426 to 427 labelled a_1(0)
424 to 425 labelled a_1(0)
445 to 423 labelled b_1(1)
444 to 445 labelled b_1(1)
442 to 443 labelled b_1(1)
443 to 444 labelled a_1(1)
443 to 435 labelled b_1(1)
440 to 441 labelled b_1(1)
441 to 442 labelled a_1(1)
441 to 457 labelled b_1(2)
439 to 440 labelled b_1(1)
438 to 439 labelled b_1(1)
436 to 437 labelled b_1(1)
437 to 438 labelled a_1(1)
435 to 436 labelled a_1(1)
456 to 441 labelled b_1(1)
455 to 456 labelled b_1(1)
453 to 454 labelled b_1(1)
454 to 455 labelled a_1(1)
454 to 435 labelled b_1(1)
451 to 452 labelled b_1(1)
452 to 453 labelled a_1(1)
452 to 457 labelled b_1(2)
450 to 451 labelled b_1(1)
449 to 450 labelled b_1(1)
447 to 448 labelled b_1(1)
448 to 449 labelled a_1(1)
446 to 447 labelled a_1(1)
467 to 441 labelled b_1(2)
466 to 467 labelled b_1(2)
464 to 465 labelled b_1(2)
465 to 466 labelled a_1(2)
465 to 435 labelled b_1(1)
462 to 463 labelled b_1(2)
463 to 464 labelled a_1(2)
463 to 457 labelled b_1(2)
461 to 462 labelled b_1(2)
460 to 461 labelled b_1(2)
458 to 459 labelled b_1(2)
459 to 460 labelled a_1(2)
457 to 458 labelled a_1(2)